STM: fischer wf

ABS: fischer-delay(del;L)

STM: fischer-delay wf

ABS: Try(e)

STM: f-try wf

ABS: Newround(e)

STM: f-newround wf

ABS: the rcv(wanted message from e1 to j)

STM: f-wanted wf

STM: f-wanted-isrcv

STM: sender-f-wanted

STM: loc-f-wanted

ABS: the rcv(free message from e1 to j)

STM: f-free wf

STM: kind-f-free

STM: loc-f-free

STM: sender-f-free

STM: f-free-isrcv

STM: time-f-free

STM: f-free-first

ABS: f-msg{$wanted,$free,$z}(es;L;e)

STM: f-msg wf

ABS: f-rel{$z,$wanted}(es;L;e1;e2)

STM: f-rel wf

STM: decidable f-rel

STM: f-rel-causal

ABS: inc-fst(p)

STM: inc-fst wf

ABS: inc-snd(p)

STM: inc-snd wf

ABS: rank(e)

STM: f-rank wf

ABS: x < y

STM: intpair-less wf

STM: intpair-less-antireflexive

ABS: round(e)

STM: f-round wf

STM: f-round-start

STM: previous-round-start

STM: round-step1

ABS: fEvent(e)

STM: f-event wf

STM: f-event-last-change

STM: f-rank-increases

STM: f-rank-unique

STM: f-inv1

STM: newround-implies

STM: newround-event

STM: taken-transition

ABS: fischer-inv(L;del;e)

STM: fischer-inv wf

STM: f-same-sender

STM: f-free-stability